es:ES, L:(E List).
L':E List
(L  L'
& L'  L
& (a, b:E. (a  L')  (b  L')  (a < b)  a before b  L')
& no_repeats(E;L')) 

latex

Definitions

as @ bs, ff, tt, i <z j, b, i z j, if b then t else f fi , nth_tl(n;as), hd(l), i  j < k, Y, ||as||, {i..j}, l[i], P  Q, P  Q, x. t(x), {T}, P  Q, xL. P(x), , A c B, P  Q, A  B, P & Q, x:A. B(x), t  T, x:A. B(x), A, e c e', x(s), Dec(P), False

Lemmas

not wf, l member-permute, not functionality wrt iff, es-causl irreflexivity, es-causle weakening, or functionality wrt iff, all functionality wrt iff, and functionality wrt iff, no repeats cons, no repeats-permute, cons before, l before member, l before append iff, es-le weakening eq, es-causle weakening locl, es-causl transitivity1, es-causl transitivity2, select member, non neg length, length wf1, append wf, l all wf2, member append, implies functionality wrt iff, decidable es-causle, es-causle wf, split-at-first, cons member, l contains cons, decidable es-E-equal, decidable l member, no repeats wf, l before wf, es-causl wf, l contains wf, no repeats nil, l member wf, nil member, l contains nil, event system wf, es-E wf